The verification of hardware or software to ensure that it cannot reach an undesired state becomes increasingly difficult as the complexity of the systems being verified increases.
In this regard verification of a system requires it to be systematically proved that the system is correct across the entire state space. With increasing complexity of systems and increasing datapath width such state space is becoming increasingly large.
Formal hardware verification, for example, involves creating a mathematical model of the hardware and performing logical reasoning on the model to determine if it satisfies or violates certain desired properties. When computationally feasible, it eliminates the need for case-by-case analysis (by simulation or emulation) since it guarantees complete coverage of the design's behavior “space”. An example of the successful deployment of formal hardware verification is combinational equivalence checking which seeks to determine if two different implementations of a combinational circuit are functionally equivalent. Formal combinational equivalence checking tools are based on highly scalable satisfiability (SAT) solvers that implicitly explore the vast input space of two combinational circuits to locate an input vector that distinguishes them or to prove that no such input vector exists thus proving their equivalence.
Formal verification of sequential hardware is conceptually similar to that of combinational hardware but significantly more complex. Simply stated, given a sequential design with a state variable vector X, a transition relation T(X, X+) that defines how a system transitions from one state to the next, an initial (reset) state predicate I(X), and a safety property P(X), the goal is to determine if all states reachable from I(X) satisfy P(X), i.e., to determine if all reachable states are safe.
Thus, the verification determines if, when starting from an initial state I and following the transition function one can ever arrive at a state outside of P. I, T and P can be determined for the system either from the software code in a software system or from the Verilog or other hardware description of a hardware system.
The safety property P, can be a collection of local assertions that must hold true in certain states, or a global predicate on all states to determine, for example, if two implementations are sequentially equivalent. Either way, to answer this question entails performing some type of reachability analysis in the design's state space, a computation that is considered to be inherently intractable except for trivially small designs. The current state of the art in sequential verification is to perform bounded reachability by unrolling the design's transition relation k times for a suitably small k. Such bounded analysis can uncover shallow bugs, i.e., violating states that can be reached in at most k cycles from reset. It is, however, incomplete, in that it is not able to find deep bugs or to prove that all reachable states are safe.
It would be desirable to be able to verify complex systems in a scalable and reliable manner.